Reviewed 7 of 10 files at r1, all commit messages.
Reviewable status: 7 of 10 files reviewed, 5 unresolved discussions (waiting on @orizi)

crates/cairo-lang-sierra-to-casm/src/invocations/array.rs line 448 at r1 (raw file):

    );
    casm_build_extend! {casm_builder,
        const popped_size = popped_size;

Suggestion:

 // Success case
 const popped_size = popped_size;

crates/cairo-lang-sierra-to-casm/src/invocations/array.rs line 486 at r1 (raw file):

        tempvar minus_length = arr_start - arr_end;
        tempvar rc = minus_length + popped_size_plus_1;
        assert rc = *(range_check++);

Why is the negative case
popped_size_plus_1 >= array_length?

shouldn't it be
array_length < popped_size
?

Suggestion:

        /// Prove that popped_size_plus_1 >= array_length        
        tempvar minus_length = arr_start - arr_end;
        tempvar rc = minus_length + popped_size_plus_1;
        assert rc = *(range_check++);

Reviewable status: 4 of 10 files reviewed, 5 unresolved discussions (waiting on @ilyalesokhin-starkware)

crates/cairo-lang-sierra/src/extensions/modules/array.rs line 633 at r1 (raw file):

it is for being repeated - but changing to i16.

crates/cairo-lang-sierra/src/extensions/modules/utils.rs line 116 at r1 (raw file):

/// Returns a fixed type array of the given type and size.
pub fn fixed_array_ty(

Done.

crates/cairo-lang-sierra-to-casm/src/invocations/array.rs line 448 at r1 (raw file):

    );
    casm_build_extend! {casm_builder,
        const popped_size = popped_size;

Done.

Reviewable status: 4 of 10 files reviewed, 5 unresolved discussions (waiting on @ilyalesokhin-starkware)

crates/cairo-lang-sierra-to-casm/src/invocations/array.rs line 391 at r1 (raw file):

since this is the bound for actual type sizes.

Reviewable status: 4 of 10 files reviewed, 5 unresolved discussions (waiting on @ilyalesokhin-starkware)

crates/cairo-lang-sierra-to-casm/src/invocations/array.rs line 486 at r1 (raw file):

Done.

Reviewed 2 of 10 files at r1, 4 of 4 files at r2, all commit messages.
Reviewable status: all files reviewed, 1 unresolved discussion (waiting on @orizi)

Reviewable status: 9 of 10 files reviewed, 1 unresolved discussion (waiting on @ilyalesokhin-starkware)

crates/cairo-lang-sierra-to-casm/src/invocations/array.rs line 487 at r2 (raw file):

        jump HasEnoughElements if has_enough_elements != 0;
        // Proving that `arr_start - arr_end + popped_size + 1 >= 0` and therefore
        // `popped_size + 1 >= arr_end - arr_end == arr.len()` ==> `arr.len() < popopped_size`.

Done.